Nuprl Lemma : update-spec1_wf2
11,40
postcript
pdf
k
:Knd,
x
:Id,
n
:top,
f
:(void
void
top).
update-spec1(
k
;
x
;
n
;
s
,
v
.
f
(
s
,
v
))
fpf((
:Knd
Id);
kz
.top)
latex
Definitions
Knd
,
t
T
,
Id
,
top
,
void
,
Type
,
x
:
A
B
(
x
)
,
isect(
A
;
x
.
B
(
x
))
,
cons(
car
;
cdr
)
,
x
.
A
(
x
)
,
<
a
,
b
>
,
[]
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
x
.
t
(
x
)
,
fpf-single(
x
;
v
)
,
update-spec1(
k
;
x
;
n
;
s
,
v
.
f
(
s
;
v
))
Lemmas
fpf-single
wf
,
top
wf
,
Id
wf
,
Knd
wf
origin
k:Knd, x:Id, n:top, f:(void
voidtop).
fpf((:Knd 
Id); kz.top) k:Knd, x:Id, n:top, f:(voidvoidtop).
fpf((:Knd Id); kz.top) TB(x)
x.A(x) B(x)x:A. B(x)
x. t(x)